(set-option :produce-proofs true)
(set-logic AUFLIA)
(declare-sort B$ 0)
(declare-sort A_set$ 0)
(declare-sort A_set_set$ 0)
(declare-sort A_set_set_set$ 0)
(declare-sort A_set_set_bool_fun$ 0)
(declare-fun a$ () B$)
(declare-fun uu$ (B$) A_set_set_bool_fun$)
(declare-fun uua$ () A_set_set_bool_fun$)
(declare-fun card$ (A_set$) Bool)
(declare-fun card$a (A_set_set_set$) Bool)
(declare-fun member$ (A_set$) A_set_set_bool_fun$)
(declare-fun collect$ (A_set_set_bool_fun$) A_set_set_set$)
(declare-fun fun_app$ (A_set_set_bool_fun$ A_set_set$) Bool)
(declare-fun partitions$ (A_set_set$ B$) Bool)
(assert (! (forall ((?v0 A_set_set$)) (! (= (fun_app$ uua$ ?v0) (and (partitions$ ?v0 a$) (forall ((?v1 A_set$)) (=> (fun_app$ (member$ ?v1) ?v0) (card$ ?v1))))) :pattern ((fun_app$ uua$ ?v0)))) :named a0))
(assert (! (forall ((?v0 B$) (?v1 A_set_set$)) (! (= (fun_app$ (uu$ ?v0) ?v1) (and (partitions$ ?v1 ?v0) (forall ((?v2 A_set$)) (=> (fun_app$ (member$ ?v2) ?v1) (card$ ?v2))))) :pattern ((fun_app$ (uu$ ?v0) ?v1)))) :named a1))
(assert (! (forall ((?v0 A_set_set_bool_fun$) (?v1 A_set_set_bool_fun$)) (=> (forall ((?v2 A_set_set$)) (= (fun_app$ ?v0 ?v2) (fun_app$ ?v1 ?v2))) (= (collect$ ?v0) (collect$ ?v1)))) :named a2))
(assert (! (forall ((?v0 B$)) (card$a (collect$ (uu$ ?v0)))) :named a3))
(assert (! (not (card$a (collect$ uua$))) :named a4))
(check-sat)
;(get-proof)